Натуральный вывод

Натуральный вывод (естественный вывод) — тип логических исчислений, использующий для доказательства утверждений правила вывода, близкие к обычным содержательным методам рассуждений.

Впервые такие исчисления созданы в 1934 году независимо Генценом и Яськовским. Наряду с исчислением секвенций относятся генценовскому типу, поскольку отталкиваются от безаксиоматического подхода (в противоположность гильбертовским исчислениям, использующим развитые наборы аксиом и минимум правил вывода). Наиболее известные системы натурального вывода — разработанные Генценом [math]\displaystyle{ \mathbf{NK} }[/math] (для классического варианта исчисления предикатов) и [math]\displaystyle{ \mathbf{NJ} }[/math] (для интуиционистского исчисления предикатов).

Правила вывода в исчислении [math]\displaystyle{ \mathbf{NJ} }[/math]:

• введение конъюнкции:

  [math]\displaystyle{ \cfrac {A \quad B}{A \wedge B} }[/math] («если верно [math]\displaystyle{ A }[/math] и [math]\displaystyle{ B }[/math], то можно заключить [math]\displaystyle{ A \wedge B }[/math]»);

• исключение конъюнкции:

  [math]\displaystyle{ \cfrac{A \wedge B}{A} }[/math] и [math]\displaystyle{ \cfrac{A \wedge B}{B} }[/math];

• введение дизъюнкции:

  [math]\displaystyle{ \cfrac{A}{A \vee B} }[/math] и [math]\displaystyle{ \cfrac{B}{A \vee B} }[/math];

• исключение дизъюнкции:

  [math]\displaystyle{ \begin{align} A \quad B \\ \vdots \; \quad \vdots \; \\ \cfrac{A \vee B \quad C \quad C}{C} \end{align} }[/math] («если верно [math]\displaystyle{ A \vee B }[/math], из [math]\displaystyle{ A }[/math] выводится [math]\displaystyle{ C }[/math] и из [math]\displaystyle{ B }[/math] выводится [math]\displaystyle{ C }[/math], то можно заключить [math]\displaystyle{ C }[/math]»);

• введение квантора всеобщности:

  [math]\displaystyle{ \cfrac{Fa}{\forall{x}Fx} }[/math];

• исключение квантора всеобщности:

  [math]\displaystyle{ \cfrac{\forall{x}Fx}{Fa} }[/math];

• введение квантора существования:

  [math]\displaystyle{ \cfrac{Fa}{\exists{x}Fx} }[/math];

• исключение квантора существования:

  [math]\displaystyle{ \begin{align} Fa \\ \vdots\; \\ \cfrac{\exists{x}Fx \quad C}{C} \end{align} }[/math];

• введение импликации:

  [math]\displaystyle{ \cfrac{B}{A \Rightarrow B} }[/math];

• исключение импликации (modus ponens):

  [math]\displaystyle{ \cfrac{A \quad A \Rightarrow B}{B} }[/math];

• введение отрицания:

  [math]\displaystyle{ \begin{align} A \\ \vdots\; \\ \cfrac{\quad \bot}{\neg A} \end{align} }[/math];

• исключение отрицания:

  [math]\displaystyle{ \cfrac{A \quad \neg A}{\bot} }[/math];

• выведение из ложного высказывания:

  [math]\displaystyle{ \cfrac{\bot}{A} }[/math].

Классическая система [math]\displaystyle{ \mathbf{NK} }[/math] получается присоединением к этим правилам вывода аксиомы [math]\displaystyle{ A \vee\neg A }[/math] или добавлением правила двойного отрицания [math]\displaystyle{ \cfrac{\neg \neg A}{A} }[/math].

Литература

• Генцен Г. Исследования логических выводов = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Идельсон А. В., Минц Г. Е. Математическая теория логического вывода / перевод А. В. Идельсона. — М.: Наука, 1967. — С. 9—76.
• Гетманова А. Д. Логика. — Книжный дом «Университет», 1998. — 480 с.
• Зиновьев А. А.  Логика высказываний и теория вывода. — Питер, 2015. — 937 с.
• Правиц Д. Натуральный вывод. Теоретико-доказательственное исследование / перевод П. Быстрова. — Лори, 1997.